Boolean Satisfiability

定义 Definition

Boolean satisfiability（布尔可满足性，常简称 SAT）：指判断一个布尔逻辑公式（由真/假变量与逻辑运算如 AND、OR、NOT 组成）是否存在某种变量赋值，使整个公式为真。它是计算机科学与逻辑、自动推理、约束求解中的核心问题；其中 SAT 是经典的 NP-完全（NP-complete） 问题之一。

发音 Pronunciation

/ˈbuːliən ˌsætɪsfæɪəˈbɪləti/

词源 Etymology

Boolean 来自英国数学家 George Boole（乔治·布尔） 的姓氏，他的研究奠定了布尔代数与现代逻辑电路/计算逻辑的基础。satisfiability 由 satisfy（使满足）+ 后缀 -ability（能力/性质）构成，表示“可被满足的性质”。合起来即“布尔公式是否可被满足（为真）”。

例句 Examples

Boolean satisfiability asks whether a logical formula can be true.
布尔可满足性研究的是：一个逻辑公式是否有可能为真。

Modern SAT solvers handle large instances of Boolean satisfiability by transforming constraints into CNF and searching for a satisfying assignment efficiently.
现代 SAT 求解器通过把约束转化为 CNF（合取范式），并高效搜索满足赋值，从而处理大规模的布尔可满足性实例。

相关词 Related Words

• Assignment
• Clause
• CNF
• Constraint
• DPLL
• Literal
• NP-Complete
• SAT
• Solver
• Three-SAT

文学与经典出处 Literary Works

• Computers and Intractability: A Guide to the Theory of NP-Completeness（Garey & Johnson）：将 SAT/可满足性问题作为 NP-完全性理论中的代表性基准问题之一进行系统讨论。
• Introduction to Algorithms（Cormen, Leiserson, Rivest, Stein；常称 CLRS）：在复杂性与归约相关内容中常以 SAT/3-SAT 作为典型例子出现。
• Handbook of Satisfiability（Biere, Heule, van Maaren, Walsh 编）：专门汇总 SAT 与可满足性研究与求解技术的权威参考书。